COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Our second approach to representing Lisp-recursive definitions
C00004 00003
C00005 ENDMK
C⊗;
	Our second approach to representing Lisp-recursive definitions
by first order formulas goes back to Goedel (1931, 1934) who showed
that primitive recursive functions could be so represented.  (Our
knowledge of Goedel's work comes from (Kleene 1951)).

.turn on "α"
.eq←0
	Kleene (1951) calls a function ⊗f %2representable%1 if there
is an arithmetic formula ⊗A with free variables ⊗x and ⊗y such
that

!!b1:	%2∀x_y.((y_=_f(x))_≡_A)%1,

where an arithmetic formula is built up from integer constants and
variables using only addition, multiplication and bounded quantification.
Goedel showed that all partial recursive functions are representable.
The proof involves Goedel numbering possible computation sequences
and showing that the relation between sequences and their elements
and the steps of the computation are all representable.

	In Lisp less machinery has to be built up, because sequences
are Lisp data, and the relation between a sequence and its elements
is given by basic Lisp functions and by the %2subexpression relation%1
defined by

!!b2:	%2x subexp y ← (x = y) ∨ ¬qat y ∧ [x subexp qa y ∨ x subexp qd y]%1.

	%2subexp%1 is the only recursive definition we shall require.